\begin{table}[htp]
\tbl{\label{tb:driverlog}   \small Comparison of time and cost of different algorithms in the DriverlogShift domain.}{
\setlength{\tabcolsep}{3pt}
\small
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|c|c|c|}
\hline
 \multirow{3}{*}{P}& \multicolumn{2}{|c|}{MiniSAT} & \multicolumn{8}{|c|}{BB-DPLL} & \multicolumn{2}{|c|}{MCC} \\
 \cline{2-13}
 & \multicolumn{2}{|c|}{no-opt} & \multicolumn{2}{|c|}{base} & \multicolumn{2}{|c|}{+h} & \multicolumn{2}{|c|}{+heu} & \multicolumn{2}{|c|}{all} &  \multicolumn{2}{|c|}{}\\
\cline{2-13}
 & T & C & T & C & T & C & T & C & T & C & T & C \\
\hline
1 & 186.4 & 2340 & 364.9 & 2110 & 899.4 & 1760 & 223.0 & 1760 & 212.0 & 1760 & 223.69 & 1760  \\ 
2 & 202.4 & 4035 & 351.9 & 1895 & 2688.7 & 895 & 202.0 & 1015 & 219.0 & 775 & 470.40 & 775  \\ 
3 & 231.1 & 4230 & 1258.8 & 2825 & 2231.9 & 2475 & 231.3 & 1395 & 231.4 & 1395 & 888.45 & 1075  \\ 
4 & 233.1 & 4715 & 290.1 & 3435 & 3721.4 & 2135 & 232.7 & 1955 & 232.8 & 1955 & 27.11 & 1835  \\ 
5 & 241.2 & 4000 & 365.1 & 2680 & 1064.1 & 2170 & 281.3 & 2480 & 639.6 & 1810 & 2225.08 & 2110 \\ 
6 & 218.5 & 2040 & 218.5 & 1930 & 218.6 & 1930 & 219.0 & 1930 & 219.0 & 1930 & 192.09 & 1930  \\ 
7 & 430.5 & 5380 & 481.5 & 4470 & 1727.3 & 3790 & 419.5 & 1370 & 419.9 & 1370 & -  & - \\ 
8 & 416.1 & 6040 & 463.8 & 3500 & 2296.3 & 4120 & 403.0 & 2270 & 403.3 & 2270 & -  & - \\ 
9 & 406.2 & 3950 & 425.1 & 3260 & 1244.6 & 3120 & 402.6 & 2010 & 403.0 & 2010 & -  & - \\ 
\hline
\end{tabular}
}
\end{table}
